YES 11.099 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule List
  ((elemIndices :: Float  ->  [Float ->  [Int]) :: Float  ->  [Float ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (\vv1 ->
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []
) (zip xs (enumFrom 0))


module Maybe where
  import qualified List
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\vv1
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices0 p vv1 = 
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

The following Lambda expression
\ab→(a,b)

is transformed to
zip0 a b = (a,b)



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule List
  ((elemIndices :: Float  ->  [Float ->  [Int]) :: Float  ->  [Float ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude



Case Reductions:
The following Case expression
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices00 p (x,i) = if p x then i : [] else []
findIndices00 p _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule List
  ((elemIndices :: Float  ->  [Float ->  [Int]) :: Float  ->  [Float ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,i if p x then i : [] else []
findIndices00 p _ []


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if p x then i : [] else []

is transformed to
findIndices000 i True = i : []
findIndices000 i False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule List
  ((elemIndices :: Float  ->  [Float ->  [Int]) :: Float  ->  [Float ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p _ []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule List
  ((elemIndices :: Float  ->  [Float ->  [Int]) :: Float  ->  [Float ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ NumRed

mainModule List
  ((elemIndices :: Float  ->  [Float ->  [Int]) :: Float  ->  [Float ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule List
  (elemIndices :: Float  ->  [Float ->  [Int])

module List where
  import qualified Maybe
import qualified Prelude

  elemIndices :: Eq a => a  ->  [a ->  [Int]
elemIndices x findIndices (== x)

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero)))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wy5100), Succ(wy400000)) → new_primPlusNat(wy5100, wy400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(wy3100), Succ(wy40100)) → new_primMulNat(wy3100, Succ(wy40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs(wy121, Succ(wy17800), Succ(wy22300), wy222) → new_psPs(wy121, wy17800, wy22300, wy222)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Succ(wy1800), wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_psPs1(wy123, Succ(wy1800), wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Succ(wy1790), wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Succ(wy1790), wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
QDP
                                    ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ UsableRulesProof
QDP
                                        ↳ QReductionProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat1(Succ(x0), x1)
new_primPlusNat1(Zero, x0)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ QReductionProof
QDP
                                            ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs2(wy141, Succ(wy1830), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs3(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_foldr1(wy43, wy410, :(wy4410, wy4411), wy141) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
new_psPs3(wy141, Succ(wy1840), wy410, Pos(wy44010), wy43, :(wy4410, wy4411)) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
new_foldr2(wy43, wy410, Float(Neg(wy44000), wy4401), wy441, wy142, wy141) → new_psPs3(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
new_psPs2(wy141, Succ(wy1830), wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_foldr2(wy43, wy410, Float(Pos(wy44000), wy4401), wy441, wy142, wy141) → new_psPs2(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
new_psPs3(wy141, Succ(wy1840), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs2(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs2(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs3(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
QDP
                                    ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs2(wy141, Succ(wy1830), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs3(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_foldr1(wy43, wy410, :(wy4410, wy4411), wy141) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
new_psPs3(wy141, Succ(wy1840), wy410, Pos(wy44010), wy43, :(wy4410, wy4411)) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
new_foldr2(wy43, wy410, Float(Neg(wy44000), wy4401), wy441, wy142, wy141) → new_psPs3(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
new_psPs2(wy141, Succ(wy1830), wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_foldr2(wy43, wy410, Float(Pos(wy44000), wy4401), wy441, wy142, wy141) → new_psPs2(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
new_psPs3(wy141, Succ(wy1840), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs2(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs2(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs3(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_psPs4(wy119, Succ(wy1750), wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Succ(wy1760), wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))
new_psPs4(wy119, Succ(wy1750), wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Succ(wy1760), wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
QDP
                                    ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ UsableRulesProof
QDP
                                        ↳ QReductionProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat1(Succ(x0), x1)
new_primPlusNat1(Zero, x0)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ QReductionProof
QDP
                                            ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))
new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr6(wy310, wy4110, wy4111, wy221, wy220) → new_foldr5(wy310, wy4111, wy220)
new_foldr5(wy310, :(wy4110, wy4111), wy125) → new_foldr6(wy310, wy4110, wy4111, new_primPlusNat0(wy125, Succ(Zero)), new_primPlusNat0(wy125, Succ(Zero)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr8(wy43, wy410, Float(Pos(wy44000), wy4401), :(wy4410, wy4411), wy144, wy143) → new_foldr8(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy143, Succ(Zero)), new_primPlusNat0(wy143, Succ(Zero)))
new_foldr8(wy43, wy410, Float(Neg(wy44000), wy4401), wy441, wy144, wy143) → new_foldr7(wy43, wy410, wy441, wy143)
new_foldr7(wy43, wy410, :(wy4410, wy4411), wy143) → new_foldr8(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy143, Succ(Zero)), new_primPlusNat0(wy143, Succ(Zero)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr10(wy310, Float(Neg(wy41000), wy4101), wy411, wy122, wy121) → new_foldr9(wy310, wy411, wy121)
new_foldr9(wy310, :(wy4110, wy4111), wy121) → new_foldr10(wy310, wy4110, wy4111, new_primPlusNat0(wy121, Succ(Zero)), new_primPlusNat0(wy121, Succ(Zero)))
new_foldr10(wy310, Float(Pos(wy41000), wy4101), wy411, wy122, wy121) → new_foldr9(wy310, wy411, wy121)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr11(wy80, wy780, :(wy8110, wy8111), wy173) → new_foldr12(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy173, Succ(Zero)), new_primPlusNat0(wy173, Succ(Zero)))
new_foldr12(wy80, wy780, Float(Pos(wy81000), wy8101), :(wy8110, wy8111), wy174, wy173) → new_foldr12(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy173, Succ(Zero)), new_primPlusNat0(wy173, Succ(Zero)))
new_foldr12(wy80, wy780, Float(Neg(wy81000), wy8101), wy811, wy174, wy173) → new_foldr11(wy80, wy780, wy811, wy173)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs6(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_foldr14(wy80, wy780, Float(Neg(wy81000), wy8101), wy811, wy172, wy171) → new_psPs7(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
new_psPs6(wy171, Succ(wy1860), wy780, Pos(wy81010), wy80, :(wy8110, wy8111)) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
new_foldr13(wy80, wy780, :(wy8110, wy8111), wy171) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
new_psPs7(wy171, Succ(wy1870), wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs6(wy171, Succ(wy1860), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_foldr14(wy80, wy780, Float(Pos(wy81000), wy8101), wy811, wy172, wy171) → new_psPs6(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
new_psPs6(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Succ(wy1870), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
QDP
                                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs6(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_foldr14(wy80, wy780, Float(Neg(wy81000), wy8101), wy811, wy172, wy171) → new_psPs7(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
new_psPs6(wy171, Succ(wy1860), wy780, Pos(wy81010), wy80, :(wy8110, wy8111)) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
new_foldr13(wy80, wy780, :(wy8110, wy8111), wy171) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
new_psPs7(wy171, Succ(wy1870), wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs6(wy171, Succ(wy1860), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_foldr14(wy80, wy780, Float(Pos(wy81000), wy8101), wy811, wy172, wy171) → new_psPs6(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
new_psPs6(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Succ(wy1870), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)

The TRS R consists of the following rules:

new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: